
module MemSaturateCounter
  #(parameter ADDR = 4,
    parameter SIZE = 4
  )

  ( input  logic saveAble,
    input  logic plus,
    input  logic [ADDR-1:0] addrSave, addrLoad,
    output logic [SIZE-1:0] dataLoad
  );

  logic saveAblePast, plusPast;
  logic [ADDR-1:0] addrSavePast;

  logic [SIZE-1:0] dataCurr;

  logic [SIZE-1:0] regs [1 << ADDR];

  assign dataLoad = regs[addrLoad];
  
  always_ff @(posedge clock) begin

    // UPDATING REGISTERS
    plusPast <= plus;
    dataCurr <= regs[addrSave];
    saveAblePast <= saveAble;
    addrSavePast <= addrSave;

    if (saveAblePast) begin

      /* if (plusPast && (dataCurr != 2'b11)) begin */
      /*   regs[addrSavePast] <= dataCurr dataCurr + 2'b1; */
      /* end */

      if (plusPast) begin
        regs[addrSavePast] <= dataCurr == 2'b11 ? dataCurr : dataCurr + 2'b1;
      end
 
      if (!plusPast && (dataCurr != 2'b0)) begin
        regs[addrSavePast] <= dataCurr - 2'b1;
      end
    
    end
  end


  `ifdef FORMAL

  logic epoch = 0;
  
  always @(posedge clock) begin

    if (reset) epoch <= 1'b1;

    if (!$past(reset) && !reset && $past(epoch) && epoch ) begin

      // SANITY CHECK
      assert(saveAblePast == $past(saveAble));
      assert(addrSavePast == $past(addrSave));
      assert(plusPast == $past(plus));

      assert(dataCurr == $past(regs[addrSave]));

      assert(regs[$past(addrSave, 2)])
      if ($past(saveAble, 2)) begin
        if ($past(plus, 2)) begin
          assert(
            (regs[$past(addrSave, 2)] == $past(regs[addrSave], 2) + 2'b1) ||
            (regs[$past(addrSave, 2)] == 2'b11)
          );
        end
      end

    end

  end

  `endif


endmodule: MemSaturateCounter